Unbounded model-checking with interpolation for regular language constraints

Abstract

We present a decision procedure for the problem of, given a set of regular expressions R 1, ..., R n , determining whether R = R 1 ∩ ... ∩ R n is empty. Our solver, revenant, finitely unrolls automata for R 1, ... , R n , encoding each as a set of propositional constraints. If a SAT solver determines satisfiability then R is non-empty. Otherwise our solver uses unbounded model checking techniques to extract an interpolant from the bounded proof. This interpolant serves as an overapproximation of R. If the solver reaches a fixed-point with the constraints remaining unsatisfiable, it has proven R to be empty. Otherwise, it increases the unrolling depth and repeats. We compare revenant with oth..